a, b, c, d:. a < b  c  d  a + c < b + d 

latex

Definitions	P & Q, T, P  Q, P  Q, , True, t  T, P  Q, x:A. B(x)
Lemmas	qadd wf, qless transitivity 1 qorder, grp op preserves lt qorder, qadd com, true wf, squash wf, grp op preserves le qorder, rationals wf, qless wf, qle wf